\label{sec:verification}

\subsection{Transformation collapse definitions}

Let us now define some useful functions for the construction of a
transformation's state space. The Graph Node Collapse function allows merging
two nodes of a graph having the same type. This function is subsequently used by
the Graph Collapse Function that recursively builds a set of all the possible
collapsed graphs from a graph.

\begin{definition}{Graph Node Collapse}

Let $\langle V,E,\tau\rangle\in TG$ be a typed graph. A graph node collapse is a
function $\chi : TG \times (V \rightarrow TG) \rightarrow \mathcal{P}(TG)$ such
that:
\begin{align*}
\chi_{\langle V,E,\tau_{V},\tau_{E}\rangle}(\iota)=\big\{&\langle
V\backslash\{y\},E',\tau_{V},\tau_{E}\backslash (y,\tau(y)) \rangle \;|\;\\ 
&x,y\in V\;\land\; \tau_{V}(x)=\tau_{V}(y)\;\land\; \iota(x) \neq
\iota(y)\;\land\; \\ &E'=\{(x,z)\;|\;(y,z)\in E\}\;\cup\\
&\qquad\,\,\{(z,x)\;|\;(z,y)\in E\}\;\cup\\
&\qquad\,\,\{(w,z)\;|\;(w,z)\in E \land w\neq y \land z\neq y\}\big\}
\end{align*}

Where $\iota$ is a function that identifies a given vertex with a typed graph.
This definition is naturally extended to transformations $TR^{s}_{t}$ by
limiting the two elements $x$ and $y$ that are collapsed to be either members
of the $Match$ pattern of the transformation or elements that are connected by
a \emph{backward link}.
\end{definition}

\begin{definition}{Graph Collapse Function}

Let $g\in TG$ be a typed graph. The graph collapse function $collapse : TG
\times (V \rightarrow TG) \rightarrow \mathcal{P}(TG)$ is recursively defined
as:
\begin{gather*}
  collapse(g,\iota) =
  \begin{cases}
    \{g\}  & \text{if } \chi_{g}(\iota)=\emptyset \\
    \chi_{g}(\iota)\;\cup\;\{g\}\;\cup\;\bigcup_{g'\in \chi_{g}(\iota)}
    collapse(g',\iota) & \text{if } \chi_{g}(\iota)\neq \emptyset\\
  \end{cases}
\end{gather*}
This definition is also naturally extended to transformation rules $TR^{s}_{t}$.
\end{definition}

%(#) collapsable is a property (proposition)
%	 of a given combinatorial state
% 	 iff we have a state which is a graph and a set of 

\begin{definition}{Collapsable}
\label{def:collapsable}

Let $g \in TG$ be a typed graph, and $G \in \mathcal{P}(TG)$ a set of typed
graphs. We say that $g$ is collapsable w.r.t. the set of typed graphs $G$
(written $collapsable(g,G)$) iff: $\forall g' \in G: \exists g''
\blacktriangleleft g\; \land g'' \cong g'$.
\end{definition}

Therefore, a typed graph $g$ is only collapsable if for each graph $g'$ of
$G$, we can find at least one subgraph of $g$ that is isomorphic to $g'$.




%(##) replaced finitude by Finiteness
\begin{proposition}{Finitude of the result of the graph collapse function}
\label{the:finitude_collapse}

Let $\langle V,E,\tau\rangle\in TG$ be a typed graph. The collapsed graph set
$collapse(\langle V,E,\tau\rangle)$ is a finite set of graphs, each graph in
that set having a finite set of nodes.
proposition.
\end{proposition}

\begin{proof}
The second part of the proposition can be proved by induction.
$\langle V,E,T\rangle$ has, by definition, a finite set of nodes.  Assuming
${\langle V',E',T'\rangle}\in collapse(\langle V,E,T\rangle)$, the result of
$\chi_{\langle V',E',T'\rangle}$ is a set of graphs where, for each of those
graphs $\langle V'',E'',T''\rangle$, $|V''|=|V'|-1$, thus making every $\langle
V'',E'',T''\rangle$ a typed graph. Given that the number of nodes with the same
type within $\langle V,E,T\rangle$ is at most $|V|$, the recursion depth of
$collapse(\langle V,E,T\rangle)$ is also at most $|V|-1$, which is the situation
where all nodes eventually collapse into one. Also, $|\chi_{\langle
V,E,T\rangle}|$ is at most $\binom{|V|}{2}$ given that nodes are collapsed two
by two. From the previous, we can build the formula that calculates the largest
possible number of elements in $|collapse(\langle V,E,T\rangle)|$:
$$1+\binom{|V|}{2}+\sum_{d=2}^{|V|-1}{\binom{|V|-d}{2}.{\binom{|V|-d+1}{2}}}$$\\
which is a finite number and thus proves the first part of the proposition.
\end{proof}

%\begin{proof}
%The second part of the proposition can be proved by induction. $\langle V,E,T\rangle$ has, by definition, a finite set of nodes.  Assuming ${\langle V',E',T'\rangle}\in collapse(\langle V,E,T\rangle)$, the result of $\chi_{\langle V',E',T'\rangle}$ is a set of graphs where, for each of those graphs $\langle V'',E'',T''\rangle$, $|V''|=|V'|-1$, thus making every $\langle V'',E'',T''\rangle$ a typed graph. Given that the number of nodes with the same type within $\langle V,E,T\rangle$ is at most $|V|$, the recursion depth of $collapse(\langle V,E,T\rangle)$ is also at most $|V|-1$, which is the situation where all nodes eventually collapse into one. Also, $|\chi_{\langle V,E,T\rangle}|$ is at most $\binom{|V|}{2}$ given that nodes are collapsed two by two. From the previous, we can build the formula that calculates the largest possible number of elements in $|collapse(\langle V,E,T\rangle)|$:
%$$1+\binom{|V|}{2}+\sum_{d=2}^{|V|-1}{\binom{|V|-d}{2}.{\binom{|V|-d+1}{2}}}$$
%which is a finite number and thus proves the first part of the proposition.$\qquad\square$
%\end{proof}

\subsection{State space}

In order to define the state space for a transformation let us start by defining
the possible combinations of transformations within a layer. More than that, we
also define a label for each of those combinations of transformation which is
used as label for the transitions in the transformation state space we build.
These labels hold the identifiers of the transformations leading to a state and
will be subsequently used to build counterexamples for properties that are
unsatisfiable.

\begin{definition}{Layer combinations}

Let $l\in Layer^{s}_{t}$ be a layer. The set of layer combinations $CL_{l}$ is obtained
as follows: $$CL_{l}=\bigcup_{tc\in \mathcal{P}(l)}\big(tc,\bigsqcup_{t\in tc}
t, \bigcup_{t\in tc} \alpha(t) \big),$$\\
where $\alpha: TG \rightarrow (V \rightarrow TG) $ is a function that returns
another function which uniquely identifies the vertices of typed graphs
as belonging to that graph , defined as: $\alpha(t) = \{ (v,t) | v \in V^{t}\}$


\end{definition}

\begin{definition}{Transformation state space}
\label{def:transf_state_space}

Let $tf=[l_{1}::\ldots::l_{n}]\in Transformation^{s}_{t}$ be a transformation.
The transformation state space $SP_{tr}\subseteq TR^{s}_{t}\times (\mathcal{P}(TR^{s}_{t})\times \mathbb{N})\times
TR^{s}_{t}$ is the least set that satisfies the following rules: 
$$\frac{(tc,ut,\iota)\in CL_{l1},tr=[l_{1}::R]\in
Transformation^{s}_{t},st\in collapse(ut,\iota)}
{\langle\emptyset,\emptyset,\emptyset,\emptyset,\emptyset,\emptyset\rangle\xlongrightarrow{tc_1}
st\in SP_{tr}}$$\\
$$\frac{\begin{array}{ll}&tr=[H::l_{k}::l_{k+1}::R]\in Transformation^{s}_{t}, st\xlongrightarrow{tc_k} st'\in
SP_{tr}\\ 
&tc\in \mathcal{P}(l_{k}),(tc',ut,\iota)\in CL_{l_{k+1}}, st''\in
collapse(st'\sqcup ut, \alpha(st') \cup \iota )\,|\,st'\end{array}}
{st'\xlongrightarrow{tc'_{k+1}} st''\in SP_{tr}}$$\\

Notice that H and R are lists. We also define $SP_{tf}^{*}$ as the transitive
closure of $SP_{tf}$. The set of states $SE_{tf}=\{st'\in
SP_{tf}\;|\;st\xlongrightarrow{tc_n} st'\in SP_{tf}\}$ is called the set of
\emph{symbolic executions} of transformation $tf$. The
$|:\mathcal{P}(TR^{s}_{t})\times TR^{s}_{t}\rightarrow \mathcal{P}(TR^{s}_{t})$
operator enforces that the backward links existing in the second parameter
transformation also exist in the transformations of the first parameter.

\end{definition}

%(##) that all transitions in the transition state space are 
%	questions about the $tc_{k}$
We now build the state space for a transformation by gathering all the
combinations of transformations for each layer, the result of collapsing them,
and building the state space as shown in Fig.~\ref{statespace}. Notice
in particular that the second inference rule in
definition~\ref{def:transf_state_space} merges the states from a previous layer
$k$ and from the current layer $k+1$. Notice also that all transitions in the
transition state space are labeled with the transformations $tc_{k}$ from the
previous $k$ layer that caused it.

%In figure~\ref{transformationmergeexample} we can observe the usefulness of the $collapse$ function while building possibilities of application of the layer 2 of the transformation in figure~\ref{dlstransformation}. Some of these possibilities have been shown in figure~\ref{dlstransformation} as the combinations of all the transformations in the layer. However, it may also occur that, for example, if we have the two transformations on the left of figure~\ref{transformationmergeexample} applied to a model, the instance of $Station$ used by the match pattern of two rules is the same. This comes from the fact that, in DSLTrans, inputs can be simultaneously consumed by several rules. In this case we can collapse the two classes in one in the transformation state space we are building. In fact, we can even go further and collapse the $Station$ classes in the apply pattern of the two rules which would mean that both $Station$ instances previously created in layer 1 (notice the backward link) are actually the same. This leads to the state shown in figure~\ref{transformationmergeexample} on the right. In fact this state is required to prove the positive property in figure~\ref{dlstransproperty}.

%More generally, the $collapse$ function is used to add additional hypothesis about the input model than the simple union of transformations as can be seen in figure~\ref{dlstransformation}. In this union all elements of the same type in the disjoint graphs of the united transformation are seen as referring to different objects in the input model --- i.e. several elements of the same type within a transformation necessarily refer to different objects in a model. By adding the collapsed transformation states to the state space we increase the amount of properties we can prove by taking into consideration all possible commonalities between transformations.

\begin{proposition}{Finitude of the transformation state space}
\label{the:finite_state_space}

Let $[l_1\ldots l_n]\in Transformation$ be a transformation. The transformation
space state $SP_{[l_1\ldots l_n]}$ is finite.
\end{proposition}

\begin{proof}
Let us start by proving by induction on the inference rules of
definition~\ref{def:transf_state_space} that the amount of states produced for
each layer $l_1\ldots l_n$ is finite. The state space for layer $l_1$ is
produced by the first rule of definition~\ref{def:transf_state_space} and
consists of the result of collapsing all the united graphs of each element of
the powerset (by definition finite) of transformations in that layer. The number
of states of the first layer is then finite because by
proposition~\ref{the:finitude_collapse} the number of transformations resulting
from a $collapse$ is finite. For the induction step, if we assume that the
amount of states produced by layer $l_k$ is finite, then the states for layer
$k+1$ should also be finite. By the second rule of
definition~\ref{def:transf_state_space}, the state space of layer $l_k$ is built
by collapsing the united  graphs of each element of the powerset of
transformations in that layer, united with each state of the previous layer.
Before collapsing we thus have $|S_{l_k}|.{2^{|l_{k+1}|}}$ states where
$|S_{l_k}|$ is the cardinality of states produced by layer $k$. Because of the
induction hypothesis $|S_{l_k}|$ is finite and thus $|S_{l_k}|.{2^{|l_{k+1}|}}$
is finite. By proposition~\ref{the:finitude_collapse} the result of the
$collapse$ function is finite and given that the restriction operator $|$ only
prunes states, the number of states produced by layer $l_{k+1}$ is finite.

Finally, the number of states in the state space $SP_{[l_1\ldots l_n]}$ can be
built by summing the number of states in each layer. Since the number of layers
in any transformation is finite by construction and the number of states in each
layer has been proved to be finite, the number of states in $SP_{[l_1\ldots
l_n]}$ is finite.
\end{proof}

The result in proposition~\ref{the:finite_state_space} is crucial since by
definition model checking can only be performed on finite state spaces.

\subsection{Property semantics}
%(##) mention the projection $match$
Let us now proceed to formally define the semantics of our properties in the
state space generated by the rules of definition~\ref{def:transf_state_space}. As
we have stated in section~\ref{sec:motivation}, a property can be
\emph{satisfiable}, \emph{unsatisfiable} or \emph{non provable}. We start with
the definition of a state in a state space (formally defined as a transformation) being
model of a property. As a reminder, each state of the state space is a symbolic
representation of a set of models given as input to the transformation being
validated and their corresponding transformations. In fact, a state holds a set of
patterns that should be instantiated in the input model --- the $match$ part of
the state --- as well as in the output model --- the $apply$ part of the state.
By validating a property at the level of the symbolic states, we validate it
for the whole set of input and output models of a given transformation. 

\begin{definition}{Model of a Property}

A transformation rule $\langle
V_{r},E_{r},\tau_{r},Match_{r},Apply_{r},Il_{r}\rangle=tr\in TR^{s}_{t}$ is a
model of a property $\langle V_p,E_p,\tau_p,Match_p,Apply_p,Il_p\rangle=P \in
Property^{s}_{t}$, written $tr \vDash^{s} P$ if:
\begin{enumerate}
\item $\langle V_p,E_p\setminus Il_p,\tau_p\rangle$ is a typed subgraph of $\langle V_r, E_r,\tau_r\rangle$
\item if $v_p\rightarrow v_{p}'\in Il_p$ then there exists $v_r\rightarrow
v_{r}'\in E_{r}^{*}$ where $\tau(v_p)=\tau(v_r)$, $\tau(v_p')=\tau(v_r')$ and
$E_{r}^{*}$ is obtained by the transitive closure of $E_{r}$.
\end{enumerate}
%Otherwise the transformation is not model of the property, which is written $TR \nvDash^{s} P$.
\end{definition}

%(##) replaced t by tr
\begin{definition}{Satisfiable Property}

Let $tf=[l_{1}::\ldots::l_{n}] \in Transformation^{s}_{t}$ be a transformation.
$tf$ \emph{satisfies} property $P\in Property^{s}_{t}$, written $tr\vDash P$,
where: $$tf\vDash P \Leftrightarrow \forall
s_0\xrightarrow{lb_0}\ldots\xrightarrow{lb_n}s_n\in SP_{tr}^{*}\;.\; (\exists
i\;.\; s_i\vDash^{s} match(P))\Rightarrow (\exists j\ge i\;.\; s_j\vDash^{s}
P)$$
\end{definition}
\begin{center}
where $s_0=\langle\emptyset,\emptyset,\emptyset,\emptyset,\emptyset,\emptyset\rangle$ and $0\leq i\leq j \leq n$.
\end{center}

%(##) for all path -> for all paths
Informally, for all paths belonging to $tr$'s state space, if the property's
$match$ pattern is found in a given state, then a subsequent state in that path
is model of the property. Note that the projection function $match$ returns the
match pattern of a property.

\begin{definition}{Unsatisfiable Property}

Let $tf=[l_{1}::\ldots::l_{n}] \in Transformation^{s}_{t}$ be a transformation.
$tf\in TR$ does \emph{not satisfy} property $P\in Property^{s}_{t}$, written
$tf\nvDash P$, where: $$tf\nvDash P \Leftrightarrow \exists
s_0\xrightarrow{lb_0}\ldots\xrightarrow{lb_n}s_n\in SP_{tf}^{*}\;.\;(\exists
i\;.\; s_i\vDash^{s} match(P))\Rightarrow (\nexists j\ge i\;.\; s_j\vDash^{s} P)$$
\begin{center}
where $s_0=\langle\emptyset,\emptyset,\emptyset,\emptyset,\emptyset,\emptyset\rangle$ and $0\leq i\leq j \leq n$.
\end{center}
The sequence $lb_0,\ldots, lb_n$ is called a \emph{counterexample} for property
$P$ in transformation $tf$.
\end{definition}

Informally, there exists a path belonging to $tr$'s state space where the
property's $match$ pattern is found in a given state, but no subsequent state
in that path is model of the property.

\begin{definition}{Non Provable Property}

Let $tf=[l_{1}::\ldots::l_{n}] \in Transformation^{s}_{t}$ be a transformation.
A property $P\in Property^{s}_{t}$ is \emph{not provable} for $tf$, written
$tf\nVDash P$, where: $$tr\nVDash P \Leftrightarrow \forall
s_0\xrightarrow{lb_0}\ldots\xrightarrow{lb_n}s_n\in SP_{tf}^{*}\;.\; (\nexists
i\;.\; s_i)\vDash^{s} match(P)$$
\begin{center}
where $s_0=\langle\emptyset,\emptyset,\emptyset,\emptyset,\emptyset,\emptyset\rangle$ and $0\leq i\leq n$.
\end{center}
\end{definition}

Again informally, the $match$ pattern can never be found in any state of the
state space of $tf$.
